(** Compute the addition between two integers *)
deferred val +? : (int * int) -> int
where (forall (x, y). pre (+?) (x, y))
 and (forall (x, y, z). post (+?) (x, y) (z) <=> z = x + y)

(** Program *)
let result =
(let (_v0, _t0) = 
   (let incr = 
      (fun x returns (y, cost) where (y = x + 1) ->
	(let (_v0, _t0) = 
	   let k = (x +? 1) in (k, 0) 
	 in
	 (_v0, (5 +? _t0)))) 
    in
    (let cost = 0 in
     (0, cost))) in
 (_v0, (7 +? _t0)))
